$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($A$$\rightarrow\mathbb{B}$), $f$:fpf($A$; $x$.$B$($x$)).
\\[0ex]fpf{-}vals(${\it eq}$; $P$; $f$) $\in$ (($x$:\{$a$:$A$$\mid$ $\uparrow$($P$($a$))\}  $\times$ $B$($x$)) List)